|
|
Static Analysis Using Facebook Infer to Find Atomicity Violations
Harmim, Dominik ; Smrčka, Aleš (referee) ; Vojnar, Tomáš (advisor)
The goal of this thesis is to propose a static analyser that detects atomicity violations. The proposed analyser Atomer is implemented as a module of Facebook Infer, which is an open-source and extendable static analysis framework that promotes efficient modular and incremental analysis. The analyser works on the level of sequences of function calls. The proposed solution is based on the assumption that sequences executed atomically once should probably be executed always atomically. The implemented analyser has been successfully verified and evaluated on both smaller programs created for testing purposes as well as publicly available benchmarks derived from real-life low-level programs.
|
|
|
Application of Genetic Algorithms and Data Mining in Noise-based Testing of Concurrent Software
Šimková, Hana ; Kofroň, Jan (referee) ; Lourenco, Joao (referee) ; Vojnar, Tomáš (advisor)
Tato práce navrhuje zlepšení výkonu testování programů použitím technik dolování z dat a genetických algoritmů při testování paralelních programů. Paralelní programování se v posledních letech stává velmi populárním i přesto, že toto programování je mnohem náročnějsí než jednodušší sekvenční a proto jeho zvýšené používání vede k podstatně vyššímu počtu chyb. Tyto chyby se vyskytují v důsledku chyb v synchronizaci jednotlivých procesů programu. Nalezení takových chyb tradičním způsobem je složité a navíc opakované spouštění těchto testů ve stejném prostředí typicky vede pouze k prohledávání stejných prokládání. V práci se využívá metody vstřikování šumu, která vystresuje program tak, že se mohou objevit některá nová chování. Pro účinnost této metody je nutné zvolit vhodné heuristiky a též i hodnoty jejich parametrů, což není snadné. V práci se využívá metod dolování z dat, genetických algoritmů a jejich kombinace pro nalezení těchto heuristik a hodnot parametrů. V práci je vedle výsledků výzkumu uveden stručný přehled dalších Technik testování paralelních programů.
|
|
|
Advanced Static Analysis of Atomicity in Concurrent Programs through Facebook Infer
Harmim, Dominik ; Rogalewicz, Adam (referee) ; Vojnar, Tomáš (advisor)
Nástroj Atomer je statický analyzátor založený na myšlence, že pokud jsou některé sekvence funkcí vícevláknového programu prováděny v některých bězích pod zámky, je pravděpodobně zamýšleno, že mají být vždy provedeny atomicky. Analyzátor Atomer se tudíž snaží takové sekvence hledat a poté zjišťovat, pro které z nich může být v některých jiných bězích programu porušena atomicita. Autor této diplomové práce ve své bakalářské práci navrhl a implementoval první verzi nástroje Atomer jako zásuvný modul aplikačního rámce Facebook Infer. V této diplomové práci je navržena nová a výrazně vylepšená verze analyzátoru Atomer. Cílem vylepšení je zvýšení jak škálovatelnosti, tak přesnosti. Kromě toho byla přidána podpora pro několik původně nepodporovaných programovacích vlastností (včetně např. možnosti analyzovat programy napsané v jazycích C++ a Java nebo podpory pro reentrantní zámky nebo stráže zámků, tzv. "lock guards"). Prostřednictvím řady experimentů (včetně experimentů s reálnými programy a reálnými chybami) se ukázalo, že nová verze nástroje Atomer je skutečně mnohem obecnější, přesnější a lépe škáluje.
|
|
|
Statická analýza v nástroji Meta Infer zaměřená na detekci souběhu nad daty
Svobodová, Lucie ; Fiedor, Jan (referee) ; Vojnar, Tomáš (advisor)
Vícevláknové programy jsou v moderních softwarových systémech využívány ke zlepšení výkonu a zvýšení efektivity. Zajištění spolehlivosti a bezpečnosti takových programů však může být náročné kvůli zvýšenému množství chyb, které se v nich vyskytují, včetně souběhu nad daty. V této práci představujeme nový statický detektor souběhu nad daty, DarC, navržený k analýze programů napsaných v jazyce C využívajících knihovnu Pthreads. Navrhovaný nástroj byl implementován jako zásuvný modul prostředí Meta Infer, což je nástroj pro statickou analýzu programů, který klade důraz na kompoziční, inkrementální a díky tomu i vysoce škálující analýzu programů. Nový analyzátor zaznamenává množinu přístupů ke sdíleným proměnným, ke kterým v analyzovaném programu došlo, spolu s informací o množině zámků uzamknutých při jednotlivých přístupech. Množina přístupů je dále použita k identifikaci dvojic přístupů, mezi nimiž by k souběhu nad daty mohlo dojít. Nástroj byl úspěšně ověřen na sadě testovacích vícevláknových programů, stejně tak jako na několika programech běžně využívaných v praxi, čímž byl ukázán jeho potenciál pro efektivní detekci souběhu nad daty v programech napsaných v programovacím jazyce C.
|
|
|
Advanced Static Analysis of Atomicity in Concurrent Programs through Facebook Infer
Harmim, Dominik ; Rogalewicz, Adam (referee) ; Vojnar, Tomáš (advisor)
Nástroj Atomer je statický analyzátor založený na myšlence, že pokud jsou některé sekvence funkcí vícevláknového programu prováděny v některých bězích pod zámky, je pravděpodobně zamýšleno, že mají být vždy provedeny atomicky. Analyzátor Atomer se tudíž snaží takové sekvence hledat a poté zjišťovat, pro které z nich může být v některých jiných bězích programu porušena atomicita. Autor této diplomové práce ve své bakalářské práci navrhl a implementoval první verzi nástroje Atomer jako zásuvný modul aplikačního rámce Facebook Infer. V této diplomové práci je navržena nová a výrazně vylepšená verze analyzátoru Atomer. Cílem vylepšení je zvýšení jak škálovatelnosti, tak přesnosti. Kromě toho byla přidána podpora pro několik původně nepodporovaných programovacích vlastností (včetně např. možnosti analyzovat programy napsané v jazycích C++ a Java nebo podpory pro reentrantní zámky nebo stráže zámků, tzv. "lock guards"). Prostřednictvím řady experimentů (včetně experimentů s reálnými programy a reálnými chybami) se ukázalo, že nová verze nástroje Atomer je skutečně mnohem obecnější, přesnější a lépe škáluje.
|
|
|
Application of Genetic Algorithms and Data Mining in Noise-based Testing of Concurrent Software
Šimková, Hana ; Kofroň, Jan (referee) ; Lourenco, Joao (referee) ; Vojnar, Tomáš (advisor)
Tato práce navrhuje zlepšení výkonu testování programů použitím technik dolování z dat a genetických algoritmů při testování paralelních programů. Paralelní programování se v posledních letech stává velmi populárním i přesto, že toto programování je mnohem náročnějsí než jednodušší sekvenční a proto jeho zvýšené používání vede k podstatně vyššímu počtu chyb. Tyto chyby se vyskytují v důsledku chyb v synchronizaci jednotlivých procesů programu. Nalezení takových chyb tradičním způsobem je složité a navíc opakované spouštění těchto testů ve stejném prostředí typicky vede pouze k prohledávání stejných prokládání. V práci se využívá metody vstřikování šumu, která vystresuje program tak, že se mohou objevit některá nová chování. Pro účinnost této metody je nutné zvolit vhodné heuristiky a též i hodnoty jejich parametrů, což není snadné. V práci se využívá metod dolování z dat, genetických algoritmů a jejich kombinace pro nalezení těchto heuristik a hodnot parametrů. V práci je vedle výsledků výzkumu uveden stručný přehled dalších Technik testování paralelních programů.
|
|
|
Static Analysis Using Facebook Infer to Find Atomicity Violations
Harmim, Dominik ; Smrčka, Aleš (referee) ; Vojnar, Tomáš (advisor)
The goal of this thesis is to propose a static analyser that detects atomicity violations. The proposed analyser Atomer is implemented as a module of Facebook Infer, which is an open-source and extendable static analysis framework that promotes efficient modular and incremental analysis. The analyser works on the level of sequences of function calls. The proposed solution is based on the assumption that sequences executed atomically once should probably be executed always atomically. The implemented analyser has been successfully verified and evaluated on both smaller programs created for testing purposes as well as publicly available benchmarks derived from real-life low-level programs.
|
|
|
Development of threads's applications in Java
ATTL, Karel
This diploma thesis is aimed at programming of multithreaded applications in Java. With Java 5 comes package java.util.concurrent, which in an important way makes developing of parallel applications easier and more effective. This work is conceived as an introduction to programming of multithreaded applications in Java and could be also used as an educational material. Theoretical introduction about processes and technological background of multitasking gives analogy to threads, at the same time it is touching on Java technology and how Java works with memory. The rest of this diploma thesis concerns practical work with threads. This topic is covered from absolute beginning, which means creating Thread objects, including advanced topics like working with package java.util.concurrent and also some problems that can appear when writing multithreaded applications.
|
guest ::
